ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da), m:,
L:(event-info(ds;da) List), z:event-info(ds;da).
spreadn(A;
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(B;
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(Tb,ksb,ib,gb,hb,ab,eb.((Ta = Tb  Type)
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c ((ksa = ksb  (Knd List))  (ia = ib  Ta))
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c ((aa
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c ((=
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c ((ab
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c (( (k:{k:Knd| (k  ksa)} decl-state(ds)
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c (( (ma-valtype(da; k)Ta))
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c  (L':(event-info(ds;da) List), k:{k:Knd| (k  ksa)} ,
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c  (s:decl-state(ds), v:ma-valtype(da; k).
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c  iseg(event-info(ds;da);
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c  iseg(append(L'; cons(<k, s, v>; []));
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c  iseg(L)
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c   (gb(k,s,v,ecl-trans-state(A; L'))
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c   (=
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c   (ga(k,s,v,ecl-trans-state(A; L'))
spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(c   ( Ta))))))
 (ecl-trans-act(ds; da; A)(m,append(L; cons(z; []))))
 (ecl-trans-act(ds; da; B)(m,append(L; cons(z; [])))) 

latex

Definitions

t  T, x:A. B(x), P  Q, False, A, A  B, , , , ma-valtype(da; k), decl-state(ds), (x  l), ecl-trans-type(A), ecl-trans-tuple{i:l}(ds; da), subtype(S; T), ecl-trans-state(v; L), top, Kind-deq, x. t(x), fpf-cap(f; eq; x; z), event-info(ds;da), b, prop{i:l}, A c B, append(as; bs), P  Q, x:A. B(x), True, T, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), spreadn(a; x,y,z.t(x;y;z)), ecl-trans-a(v), ecl-trans-ks(v), ecl-trans-act(ds; da; A), guard(T), sq_type(T), P  Q, ge(i; j), ||as||, suptype(S; T), iseg(T; l1; l2), fpf(A; a.B(a)), Id, Knd, b, deq-member(eq; x; L), Unit, if b then t else f fi , list_accum(x,a.f(x;a); y; l), x,y. t(x;y), ecl-trans-state-from(v; z; L), ecl-trans-init(v)

Lemmas

append-cancellation-right, list accum wf, list accum functionality, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, not wf, Id wf, fpf wf, ecl-trans-tuple wf, iseg wf, le wf, length wf1, non neg length, cons one one, Knd sq, ecl-trans-act wf, squash wf, true wf, append wf, event-info wf, assert wf, fpf-cap wf, Kind-deq wf, top wf, ecl-trans-state wf, nat wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bool wf, nat plus wf, subtype rel self